Problem:
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(++(x,y),z) -> ++(x,++(y,z))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    .1(1,4) -> 4,3
    .1(2,7) -> 4,3
    .1(1,7) -> 4,3
    .1(2,4) -> 4,3
    ++1(1,2) -> 7*
    ++1(2,1) -> 4*
    ++1(1,1) -> 4*
    ++1(2,2) -> 4*
    ++0(1,2) -> 3*
    ++0(2,1) -> 3*
    ++0(1,1) -> 3*
    ++0(2,2) -> 3*
    nil0() -> 1*
    .0(1,2) -> 2*
    .0(2,1) -> 2*
    .0(1,1) -> 2*
    .0(2,2) -> 2*
    1 -> 4,3
    2 -> 4,7,3
  problem:
   
  Qed